$\forall$${\it es}$:ES, $k$:Knd, $l$:IdLnk, ${\it tg}$:Id, $B$, $T$:Type, $f$:(state@source($l$)$\rightarrow$$B$$\rightarrow$$T$).
\\[0ex]only $k$($v$):$B$ sends [${\it tg}$,$f$($s$,$v$)] : $T$ on $l$ $\in$ Prop